\chapter{Entries}

This chapter provides manual entries for pre-defined \ML{} identifiers
in the \HOL{} system.  These include: general-purpose functions, such
as functions for list processing, arithmetic, input/output, and
interface configuration; functions for processing the types and terms
of the \HOL{} logic, for setting up theories, and for using the
subgoal package; primitive and derived forward inference rules; and
tactics and tacticals.  The arrangement is alphabetical.  If an
entry's title box includes a parenthesised word to the right, this
identifies the ML structure where that identifier is bound.
The interactive system starts with some structures already present,
others will need to be \texttt{load}-ed first.

%%% Local Variables:
%%% mode: plain-tex
%%% TeX-master: "reference"
%%% End:
